High-level programming languages such as Java, C++, and C# are generally used to produce source codes. These source codes are optimized and compiled by compilers to assembly language code before they are executed on machines. Compilers may contain program errors, which are also known as bugs, which may cause the compilers to compile safe source code to unsafe assembly language code. Programs based on unsafe assembly language code may malfunction and/or cause other programs to malfunction. In some instances, the safety of assembly language code may be verified after compilation by “type checking” mechanisms, provided that the source code is compiled into the assembly language code by a special type of compilers known as “type-preserving” compilers. A “type-preserving” compiler generates the “evidence” needed by the “type-checking” mechanisms by transforming a well-typed source code into a well-typed assembly language code, preserving the types in the intermediate code during each compilation phase between the source code and assembly language code. “Type checking” relies on the premise that a specific type indicates a set of values or expressions that have the same sort of generic meaning or intended purpose.